Section: New Results

New Formal Languages and their Implementations

LNT is a next generation formal description language for asynchronous concurrent systems, which attempts to combine the best features of imperative programming languages and value-passing process algebras. LNT is increasingly used by CONVECS for industrial case studies and applications (see § 6.5) and serves also in university courses on concurrency, in particular at ENSIMAG (Grenoble) and at Saarland University.

Translation from LNT to LOTOS

Participants : Hubert Garavel, Frédéric Lang, Wendelin Serwe.

The move towards “safer” LNT exceptions initiated in 2016 has been completed in 2017: the two concepts of gates and exceptions have been unified in both LNT processes and LNT functions. The static semantics of LNT no longer requires that variables and exceptions share the same name space.

LNT now permits simple loops (of the form “loop ... end loop”, without loop label nor “while” condition) in LNT functions, as well as in LNT processes.

The pragma names “comparedby”, “external”, “implementedby”, “iteratedby”, “printedby”, and “representedby” are no longer reserved LNT keywords, meaning that it is now permitted to declare LNT identifiers having these names. Two new type pragmas “!card” and “!bits” have been added to specify the maximum number of values and the number of bits to be used when storing the values of a given type in “hash-consing” tables.

The LPP preprocessor and the LNT2LOTOS translator, which implement the LNT language, have been enhanced in many ways. In addition to 9 bug fixes, the following enhancements have been made:

• LPP now implements LNT character strings more concisely.

• LPP automatically adds the “.lnt” extension to input and output files if this extension is missing.

• The algorithm that computes which LNT gates are used in each function or process has been made more precise, and LNT2LOTOS now warns about gates that are declared but never used.

• LNT2LOTOS performs stricter compile-time checks that produce dedicated error messages, rather than generating invalid LOTOS code that was subsequently rejected by CAESAR and/or CAESAR.ADT. Also, several error messages displayed by LNT2LOTOS during its static-analysis phases have been enhanced.

• The translation from LNT functions to LOTOS operations has been significantly improved by eliminating unreachable or redundant LOTOS equations, removing unused auxiliary LOTOS operations, simplifying the premises of certain LOTOS equations, factorizing identical assignments in “if-then-else” instructions, and optimizing long sequences of assignments intertwined with assertions. Thus, LNT2LOTOS is now faster, uses less memory, generates more compact LOTOS code, and can compile larger LNT specifications that could not be handled before.

The LNT2LOTOS Reference Manual, which contains the definition of the LNT language, has been revised, enriched, and simplified in many ways. A paper presenting the historical background and motivation behind the definition of LNT was published in an international conference [18].

NUPN

Participant : Hubert Garavel.

Nested-Unit Petri Nets (NUPNs) is an upward-compatible extension of P/T nets, which are enriched with structural information on their concurrent structure. Such additional information can easily be produced when NUPNs are generated from higher-level specifications (e.g., process calculi); quite often, such information allows logarithmic reductions in the number of bits required to represent states, thus enabling verification tools to perform better. The principles of NUPNs are exposed in [29] and its PNML representation is described here (http://mcc.lip6.fr/nupn.php).

In 2017, we studied an abstraction called place fusion, which takes advantage of the compositional, hierarchical structure of NUPNs. We formulated key theorems stating which properties are preserved or not under this abstraction. On the practical side, our collection of NUPN models grew to more than $8000$ benchmarks. Statistical studies were done on this collection to estimate the compression factor permitted by the NUPN model. A journal article providing an overview of NUPNs was written.

The NUPN model has been adopted by the Model Checking Contest and implemented in ten different tools developed in four countries. In 2017, the NUPN model was also adopted for the parallel problems of the RERS'2017 (Rigorous Examination of Reactive Systems) challenge (http://www.rers-challenge.org).

Analysis of BPMN via Translation to LNT

Participants : Ajay Muroor Nadumane, Gwen Salaün.

Business process modeling is an important concern in companies and organizations. Formal analysis techniques are crucial to detect semantic issues in the corresponding models, or to help with their refactoring and evolution. However, business process development frameworks often fall short when it comes to go beyond simulation or syntactic checking of the models. To ensure a more robust development of business processes, we developed the VBPMN verification framework. It features several techniques for the automatic analysis of business processes modeled using BPMN, the de facto standard for business process modeling.

The business processes, described using a Web application compliant with BPMN 2.0, are transformed into an intermediate format called PIF (Process Intermediate Format). Then, from the PIF descriptions, models in LNT and model-specific verification scripts in SVL are generated. In the end, CADP is used to check either for functional properties of a given business process, or for the correctness of the evolution of a business process into another one. This latter kind of verification supported by VBPMN is particularly helpful in order to improve a process w.r.t. certain optimization criteria. A paper presenting these results was published in an international conference [16].

Translation of Term Rewrite Systems

Participants : Hubert Garavel, Lina Marsso.

We pursued the development undertaken in 2015 of a software platform for systematically comparing the performance of rewrite engines and pattern-matching implementations in algebraic specification and functional programming languages. Our platform reuses the benchmarks of the three Rewrite Engine Competitions (2006, 2009, and 2010). Such benchmarks are term-rewrite systems expressed in a simple formalism named REC, for which we developed automated translators that convert REC benchmarks into many languages, among which AProVE, Clean, Haskell, LNT, LOTOS, Maude, mCRL, MLTON, OCAML, Opal, Rascal, Scala, SML-NJ, Stratego/XT, and Tom.

In 2017, we revised and enhanced the largest REC benchmark, the MAA (Message Authenticator Algorithm), a Message Authentication Code used for financial transactions (ISO 8731-2) between 1987 and 2002. This model (13 sorts, 18 constructors, 644 non-constructors, and 684 rewrite rules) was proven to be confluent, and terminating. Implementations in thirteen different languages have been automatically derived from this model and used to validate 200 official test vectors for the MAA. These results led to a publication in an international conference [14].

We also corrected and/or enhanced several of the existing REC translators (e.g., Clean) and added support of CafeOBJ and compiled OCAML. A scientific paper on this study has been prepared.

Other Language Developments

Participants : Hubert Garavel, Frédéric Lang, Radu Mateescu, Wendelin Serwe.

The ability to compile and verify formal specifications with complex, user-defined operations and data structures is a key feature of the CADP toolbox since its very origins.

In 2017, we brought various enhancements to several compilers handling formal specification languages (LOTOS, MCL, XTL, and GRL):

• A buffer overflow and two out-of-bound array accesses have been corrected in both CAESAR and CAESAR.ADT. Two memory allocation bugs have also been corrected in CAESAR.ADT. The latter tool now generates C code that gives better diagnostic when the evaluation of a constant fails at run time (e.g., when it triggers an exception signal, or exhausts the stack or heap memory).

• In addition to two bug fixes, the warning and error messages displayed by MCL_EXPAND and XTL_EXPAND have been made more precise and stringent. The XTL libraries “walk” and “walk_nice” have been modified not to trigger the extra warnings recently introduced.

• The GRL2LNT translator takes as input a formal description in GRL of a GALS system and generates an equivalent LNT specification. A new version 1.1 of GRL2LNT has been released, which corrects a bug concerning the LNT code generated by the “-merge ” option.

H. Garavel pursued the study of the most suitable axiomatization of signed integers undertaken in 2016. He reviewed a tenth of such Peano-like axiom systems, which he classified and evaluated according to complexity and efficiency criteria. These results have been published in an international conference [13].